\begin{tabbing}
state ${\it ds}$
\\[0ex]$k$:$A$ sends [${\it tg}$, $e$.$f$($e$):$B$] on $l$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:E. kind($e$) $=$ rcv($l$,${\it tg}$) $\Rightarrow$ valtype($e$) $\subseteq\rho$ $B$)\+
\\[0ex]\& ($\forall$$x$:Id. vartype(source($l$);$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]\& ($\forall$$e$:E. kind($e$) $=$ $k$ $\Rightarrow$ loc($e$) $=$ source($l$) $\Rightarrow$ valtype($e$) $\subseteq\rho$ $A$)
\\[0ex]\& \=$\forall$$e$@source($l$).\+
\\[0ex]kind($e$) $=$ $k$ $\Rightarrow$ isl($f$($e$)) $\Rightarrow$ ($\exists$${\it e'}$:E. kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) \& sender(${\it e'}$) $=$ $e$)
\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex]kind(${\it e'}$) $=$ rcv($l$,${\it tg}$)
\\[0ex]$\Rightarrow$ kind(sender(${\it e'}$)) $=$ $k$ \& isl($f$(sender(${\it e'}$))) \& val(${\it e'}$) $=$ outl($f$(sender(${\it e'}$))))
\-\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex]kind(${\it e'}$) $=$ rcv($l$,${\it tg}$)
\\[0ex]$\Rightarrow$ ($\forall$${\it e''}$:E. kind(${\it e''}$) $=$ rcv($l$,${\it tg}$) $\Rightarrow$ sender(${\it e''}$) $=$ sender(${\it e'}$) $\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$))
\-\-\-
\end{tabbing}